﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace Aima.NET.Test.Core.Logic.FOL.Inference
{
    using Aima.Core.Logic.FOL.Inference;
    using Aima.Core.Logic.FOL.Inference.Proof;
    using Aima.Core.Logic.FOL.KB;
    using Aima.Core.Logic.FOL.Parsing.AST;

    using Microsoft.VisualStudio.TestTools.UnitTesting;

    public abstract class CommonFOLInferenceProcedureTests
    {

        //
        // Protected Methods
        //
        protected void TestDefiniteClauseKbKingsQueryCriminalXFalse(
                IInferenceProcedure infp)
        {
            FOLKnowledgeBase kkb = FOLKnowledgeBaseFactory.CreateKingsKnowledgeBase(infp);
            IList<ITerm> terms = new List<ITerm> { new Variable("x") };
            var query = new Predicate("Criminal", terms);
            IInferenceResult answer = kkb.Ask(query);
            Assert.IsTrue(null != answer);
            Assert.IsTrue(answer.IsPossiblyFalse());
            Assert.IsFalse(answer.IsTrue());
            Assert.IsFalse(answer.IsUnknownDueToTimeout());
            Assert.IsFalse(answer.IsPartialResultDueToTimeout());
            Assert.IsTrue(0 == answer.GetProofs().Count);
        }

        protected void TestDefiniteClauseKbKingsQueryRichardEvilFalse(
                IInferenceProcedure infp)
        {
            FOLKnowledgeBase kkb = FOLKnowledgeBaseFactory
                    .CreateKingsKnowledgeBase(infp);
            IList<ITerm> terms = new List<ITerm>();
            terms.Add(new Constant("Richard"));
            var query = new Predicate("Evil", terms);
            IInferenceResult answer = kkb.Ask(query);
            Assert.IsTrue(null != answer);
            Assert.IsTrue(answer.IsPossiblyFalse());
            Assert.IsFalse(answer.IsTrue());
            Assert.IsFalse(answer.IsUnknownDueToTimeout());
            Assert.IsFalse(answer.IsPartialResultDueToTimeout());
            Assert.IsTrue(0 == answer.GetProofs().Count);
        }

        protected void TestDefiniteClauseKbKingsQueryJohnEvilSucceeds(
                IInferenceProcedure infp)
        {
            FOLKnowledgeBase kkb = FOLKnowledgeBaseFactory
                    .CreateKingsKnowledgeBase(infp);
            IList<ITerm> terms = new List<ITerm> { new Constant("John") };
            var query = new Predicate("Evil", terms);
            IInferenceResult answer = kkb.Ask(query);

            Assert.IsTrue(null != answer);
            Assert.IsFalse(answer.IsPossiblyFalse());
            Assert.IsTrue(answer.IsTrue());
            Assert.IsFalse(answer.IsUnknownDueToTimeout());
            Assert.IsFalse(answer.IsPartialResultDueToTimeout());
            Assert.IsTrue(1 == answer.GetProofs().Count);
            Assert.IsTrue(0 == answer.GetProofs()[0].GetAnswerBindings()
                    .Count);
        }

        protected void TestDefiniteClauseKbKingsQueryEvilXReturnsJohnSucceeds(
                IInferenceProcedure infp)
        {
            FOLKnowledgeBase kkb = FOLKnowledgeBaseFactory
                    .CreateKingsKnowledgeBase(infp);
            IList<ITerm> terms = new List<ITerm> { new Variable("x") };
            var query = new Predicate("Evil", terms);
            IInferenceResult answer = kkb.Ask(query);

            Assert.IsTrue(null != answer);
            Assert.IsFalse(answer.IsPossiblyFalse());
            Assert.IsTrue(answer.IsTrue());
            Assert.IsFalse(answer.IsUnknownDueToTimeout());
            Assert.IsFalse(answer.IsPartialResultDueToTimeout());
            Assert.IsTrue(1 == answer.GetProofs().Count);
            Assert.IsTrue(1 == answer.GetProofs()[0].GetAnswerBindings()
                    .Count);
            Assert.AreEqual(new Constant("John"), answer.GetProofs()[0]
                    .GetAnswerBindings()[new Variable("x")]);
        }

        protected void TestDefiniteClauseKbKingsQueryKingXReturnsJohnAndRichardSucceeds(
                IInferenceProcedure infp) {
        FOLKnowledgeBase kkb = FOLKnowledgeBaseFactory
                .CreateKingsKnowledgeBase(infp);
        IList<ITerm> terms = new List<ITerm> { new Variable("x") };
            Predicate query = new Predicate("King", terms);
        IInferenceResult answer = kkb.Ask(query);

        Assert.IsTrue(null != answer);
        Assert.IsFalse(answer.IsPossiblyFalse());
        Assert.IsTrue(answer.IsTrue());
        Assert.IsFalse(answer.IsUnknownDueToTimeout());
        Assert.IsFalse(answer.IsPartialResultDueToTimeout());
        Assert.IsTrue(2 == answer.GetProofs().Count);
        Assert.IsTrue(1 == answer.GetProofs()[0].GetAnswerBindings()
                .Count);
        Assert.IsTrue(1 == answer.GetProofs()[1].GetAnswerBindings()
                .Count);

        bool gotJohn, gotRichard;
        gotJohn = gotRichard = false;
        Constant cJohn = new Constant("John");
        Constant cRichard = new Constant("Richard");
        foreach (IProof p in answer.GetProofs()) {
            IDictionary<Variable, ITerm> ans = p.GetAnswerBindings();
            Assert.AreEqual(1, ans.Count);
            if (cJohn.Equals(ans[new Variable("x")])) {
                gotJohn = true;
            }
            if (cRichard.Equals(ans[new Variable("x")])) {
                gotRichard = true;
            }
        }
        Assert.IsTrue(gotJohn);
        Assert.IsTrue(gotRichard);
    }

        protected void TestDefiniteClauseKbWeaponsQueryCriminalXReturnsWestSucceeds(
                IInferenceProcedure infp)
        {
            FOLKnowledgeBase wkb = FOLKnowledgeBaseFactory
                    .CreateWeaponsKnowledgeBase(infp);
            IList<ITerm> terms = new List<ITerm> { new Variable("x") };
            var query = new Predicate("Criminal", terms);

            IInferenceResult answer = wkb.Ask(query);

            Assert.IsTrue(null != answer);
            Assert.IsFalse(answer.IsPossiblyFalse());
            Assert.IsTrue(answer.IsTrue());
            Assert.IsFalse(answer.IsUnknownDueToTimeout());
            Assert.IsFalse(answer.IsPartialResultDueToTimeout());
            Assert.IsTrue(1 == answer.GetProofs().Count);
            Assert.IsTrue(1 == answer.GetProofs()[0].GetAnswerBindings()
                    .Count);
            Assert.AreEqual(new Constant("West"), answer.GetProofs()[0]
                    .GetAnswerBindings()[new Variable("x")]);
        }

        protected void TestHornClauseKbRingOfThievesQuerySkisXReturnsNancyRedBertDrew(
                IInferenceProcedure infp) {
        FOLKnowledgeBase rotkb = FOLKnowledgeBaseFactory
                .CreateRingOfThievesKnowledgeBase(infp);
        IList<ITerm> terms = new List<ITerm> { new Variable("x") };
        var query = new Predicate("Skis", terms);

        IInferenceResult answer = rotkb.Ask(query);

        Assert.IsTrue(null != answer);
        Assert.IsFalse(answer.IsPossiblyFalse());
        Assert.IsTrue(answer.IsTrue());
        Assert.IsFalse(answer.IsUnknownDueToTimeout());
        // DB can expand infinitely so is only partial.
        Assert.IsTrue(answer.IsPartialResultDueToTimeout());
        Assert.AreEqual(4, answer.GetProofs().Count);
        Assert.AreEqual(1, answer.GetProofs()[0].GetAnswerBindings()
                .Count);
        Assert.AreEqual(1, answer.GetProofs()[1].GetAnswerBindings()
                .Count);
        Assert.AreEqual(1, answer.GetProofs()[2].GetAnswerBindings()
                .Count);
        Assert.AreEqual(1, answer.GetProofs()[3].GetAnswerBindings()
                .Count);

        IList<Constant> expected = new List<Constant>
            { new Constant("Nancy"), new Constant("Red"), new Constant("Bert"), new Constant("Drew") };
            foreach (IProof p in answer.GetProofs()) {
            expected.Remove((Constant) p.GetAnswerBindings()[new Variable("x")]);
        }
        Assert.AreEqual(0, expected.Count);
    }

        protected void TestFullFOLKBLovesAnimalQueryKillsCuriosityTunaSucceeds(
                IInferenceProcedure infp, bool expectedToTimeOut)
        {
            FOLKnowledgeBase akb = FOLKnowledgeBaseFactory
                    .CreateLovesAnimalKnowledgeBase(infp);
            IList<ITerm> terms = new List<ITerm> { new Constant("Curiosity"), new Constant("Tuna") };
            var query = new Predicate("Kills", terms);

            IInferenceResult answer = akb.Ask(query);
            Assert.IsTrue(null != answer);
            if (expectedToTimeOut)
            {
                Assert.IsFalse(answer.IsPossiblyFalse());
                Assert.IsFalse(answer.IsTrue());
                Assert.IsTrue(answer.IsUnknownDueToTimeout());
                Assert.IsFalse(answer.IsPartialResultDueToTimeout());
                Assert.IsTrue(0 == answer.GetProofs().Count);
            }
            else
            {
                Assert.IsFalse(answer.IsPossiblyFalse());
                Assert.IsTrue(answer.IsTrue());
                Assert.IsFalse(answer.IsUnknownDueToTimeout());
                Assert.IsFalse(answer.IsPartialResultDueToTimeout());
                Assert.IsTrue(1 == answer.GetProofs().Count);
                Assert.IsTrue(0 == answer.GetProofs()[0]
                        .GetAnswerBindings().Count);
            }
        }

        protected void TestFullFOLKBLovesAnimalQueryNotKillsJackTunaSucceeds(
                IInferenceProcedure infp, bool expectedToTimeOut)
        {
            FOLKnowledgeBase akb = FOLKnowledgeBaseFactory
                    .CreateLovesAnimalKnowledgeBase(infp);
            IList<ITerm> terms = new List<ITerm> { new Constant("Jack"), new Constant("Tuna") };
            var query = new NotSentence(new Predicate("Kills", terms));

            IInferenceResult answer = akb.Ask(query);

            Assert.IsTrue(null != answer);
            if (expectedToTimeOut)
            {
                Assert.IsFalse(answer.IsPossiblyFalse());
                Assert.IsFalse(answer.IsTrue());
                Assert.IsTrue(answer.IsUnknownDueToTimeout());
                Assert.IsFalse(answer.IsPartialResultDueToTimeout());
                Assert.IsTrue(0 == answer.GetProofs().Count);
            }
            else
            {
                Assert.IsFalse(answer.IsPossiblyFalse());
                Assert.IsTrue(answer.IsTrue());
                Assert.IsFalse(answer.IsUnknownDueToTimeout());
                Assert.IsFalse(answer.IsPartialResultDueToTimeout());
                Assert.IsTrue(1 == answer.GetProofs().Count);
                Assert.IsTrue(0 == answer.GetProofs()[0]
                        .GetAnswerBindings().Count);
            }
        }

        protected void TestFullFOLKBLovesAnimalQueryKillsJackTunaFalse(
                IInferenceProcedure infp, bool expectedToTimeOut)
        {
            FOLKnowledgeBase akb = FOLKnowledgeBaseFactory
                    .CreateLovesAnimalKnowledgeBase(infp);
            IList<ITerm> terms = new List<ITerm> { new Constant("Jack"), new Constant("Tuna") };
            var query = new Predicate("Kills", terms);

            IInferenceResult answer = akb.Ask(query);

            Assert.IsTrue(null != answer);
            if (expectedToTimeOut)
            {
                Assert.IsFalse(answer.IsPossiblyFalse());
                Assert.IsFalse(answer.IsTrue());
                Assert.IsTrue(answer.IsUnknownDueToTimeout());
                Assert.IsFalse(answer.IsPartialResultDueToTimeout());
                Assert.IsTrue(0 == answer.GetProofs().Count);
            }
            else
            {
                Assert.IsTrue(answer.IsPossiblyFalse());
                Assert.IsFalse(answer.IsTrue());
                Assert.IsFalse(answer.IsUnknownDueToTimeout());
                Assert.IsFalse(answer.IsPartialResultDueToTimeout());
                Assert.IsTrue(0 == answer.GetProofs().Count);
            }
        }

        protected void TestEqualityAxiomsKBabcAEqualsCSucceeds(
                IInferenceProcedure infp)
        {
            FOLKnowledgeBase akb = FOLKnowledgeBaseFactory
                    .CreateAbcEqualityKnowledgeBase(infp, true);

            var query = new TermEquality(new Constant("A"), new Constant(
                    "C"));

            IInferenceResult answer = akb.Ask(query);

            Assert.IsTrue(null != answer);
            Assert.IsFalse(answer.IsPossiblyFalse());
            Assert.IsTrue(answer.IsTrue());
            Assert.IsFalse(answer.IsUnknownDueToTimeout());
            Assert.IsFalse(answer.IsPartialResultDueToTimeout());
            Assert.IsTrue(1 == answer.GetProofs().Count);
            Assert.IsTrue(0 == answer.GetProofs()[0].GetAnswerBindings()
                    .Count);
        }

        protected void TestEqualityAndSubstitutionAxiomsKBabcdFfaSucceeds(
                IInferenceProcedure infp)
        {
            FOLKnowledgeBase akb = FOLKnowledgeBaseFactory
                    .CreateAbcdEqualityAndSubstitutionKnowledgeBase(infp, true);

            IList<ITerm> terms = new List<ITerm> { new Constant("A") };
            var fa = new Function("F", terms);
            terms = new List<ITerm> { fa };
            var query = new TermEquality(new Function("F", terms),
                    new Constant("A"));

            IInferenceResult answer = akb.Ask(query);

            Assert.IsTrue(null != answer);
            Assert.IsFalse(answer.IsPossiblyFalse());
            Assert.IsTrue(answer.IsTrue());
            Assert.IsFalse(answer.IsUnknownDueToTimeout());
            Assert.IsFalse(answer.IsPartialResultDueToTimeout());
            Assert.IsTrue(1 == answer.GetProofs().Count);
            Assert.IsTrue(0 == answer.GetProofs()[0].GetAnswerBindings()
                    .Count);
        }

        protected void TestEqualityAndSubstitutionAxiomsKBabcdPdSucceeds(
                IInferenceProcedure infp)
        {
            FOLKnowledgeBase akb = FOLKnowledgeBaseFactory
                    .CreateAbcdEqualityAndSubstitutionKnowledgeBase(infp, true);

            IList<ITerm> terms = new List<ITerm> { new Constant("D") };
            var query = new Predicate("P", terms);

            IInferenceResult answer = akb.Ask(query);

            Assert.IsTrue(null != answer);
            Assert.IsFalse(answer.IsPossiblyFalse());
            Assert.IsTrue(answer.IsTrue());
            Assert.IsFalse(answer.IsUnknownDueToTimeout());
            Assert.IsFalse(answer.IsPartialResultDueToTimeout());
            Assert.IsTrue(1 == answer.GetProofs().Count);
            Assert.IsTrue(0 == answer.GetProofs()[0].GetAnswerBindings()
                    .Count);
        }

        protected void TestEqualityAndSubstitutionAxiomsKBabcdPffaSucceeds(
                IInferenceProcedure infp, bool expectedToTimeOut)
        {
            FOLKnowledgeBase akb = FOLKnowledgeBaseFactory
                    .CreateAbcdEqualityAndSubstitutionKnowledgeBase(infp, true);

            IList<ITerm> terms = new List<ITerm> { new Constant("A") };
            var fa = new Function("F", terms);
            terms = new List<ITerm> { fa };
            var ffa = new Function("F", terms);
            terms = new List<ITerm> { ffa };
            var query = new Predicate("P", terms);

            IInferenceResult answer = akb.Ask(query);

            if (expectedToTimeOut)
            {
                Assert.IsFalse(answer.IsPossiblyFalse());
                Assert.IsFalse(answer.IsTrue());
                Assert.IsTrue(answer.IsUnknownDueToTimeout());
                Assert.IsFalse(answer.IsPartialResultDueToTimeout());
                Assert.IsTrue(0 == answer.GetProofs().Count);
            }
            else
            {
                Assert.IsTrue(null != answer);
                Assert.IsFalse(answer.IsPossiblyFalse());
                Assert.IsTrue(answer.IsTrue());
                Assert.IsFalse(answer.IsUnknownDueToTimeout());
                Assert.IsFalse(answer.IsPartialResultDueToTimeout());
                Assert.IsTrue(1 == answer.GetProofs().Count);
                Assert.IsTrue(0 == answer.GetProofs()[0]
                        .GetAnswerBindings().Count);
            }
        }

        protected void TestEqualityNoAxiomsKBabcAEqualsCSucceeds(
                IInferenceProcedure infp, bool expectedToFail)
        {
            FOLKnowledgeBase akb = FOLKnowledgeBaseFactory
                    .CreateAbcEqualityKnowledgeBase(infp, false);

            var query = new TermEquality(new Constant("A"), new Constant(
                    "C"));

            IInferenceResult answer = akb.Ask(query);

            Assert.IsTrue(null != answer);
            if (expectedToFail)
            {
                Assert.IsTrue(answer.IsPossiblyFalse());
                Assert.IsFalse(answer.IsTrue());
                Assert.IsFalse(answer.IsUnknownDueToTimeout());
                Assert.IsFalse(answer.IsPartialResultDueToTimeout());
                Assert.IsTrue(0 == answer.GetProofs().Count);
            }
            else
            {
                Assert.IsFalse(answer.IsPossiblyFalse());
                Assert.IsTrue(answer.IsTrue());
                Assert.IsFalse(answer.IsUnknownDueToTimeout());
                Assert.IsFalse(answer.IsPartialResultDueToTimeout());
                Assert.IsTrue(1 == answer.GetProofs().Count);
                Assert.IsTrue(0 == answer.GetProofs()[0]
                        .GetAnswerBindings().Count);
            }
        }

        protected void TestEqualityAndSubstitutionNoAxiomsKBabcdFfaSucceeds(
                IInferenceProcedure infp, bool expectedToFail)
        {
            FOLKnowledgeBase akb = FOLKnowledgeBaseFactory
                    .CreateAbcdEqualityAndSubstitutionKnowledgeBase(infp, false);

            IList<ITerm> terms = new List<ITerm> { new Constant("A") };
            var fa = new Function("F", terms);
            terms = new List<ITerm> { fa };
            var query = new TermEquality(new Function("F", terms),
                    new Constant("A"));

            IInferenceResult answer = akb.Ask(query);

            Assert.IsTrue(null != answer);
            if (expectedToFail)
            {
                Assert.IsTrue(answer.IsPossiblyFalse());
                Assert.IsFalse(answer.IsTrue());
                Assert.IsFalse(answer.IsUnknownDueToTimeout());
                Assert.IsFalse(answer.IsPartialResultDueToTimeout());
                Assert.IsTrue(0 == answer.GetProofs().Count);
            }
            else
            {
                Assert.IsFalse(answer.IsPossiblyFalse());
                Assert.IsTrue(answer.IsTrue());
                Assert.IsFalse(answer.IsUnknownDueToTimeout());
                Assert.IsFalse(answer.IsPartialResultDueToTimeout());
                Assert.IsTrue(1 == answer.GetProofs().Count);
                Assert.IsTrue(0 == answer.GetProofs()[0]
                        .GetAnswerBindings().Count);
            }
        }

        protected void TestEqualityAndSubstitutionNoAxiomsKBabcdPdSucceeds(
                IInferenceProcedure infp, bool expectedToFail)
        {
            FOLKnowledgeBase akb = FOLKnowledgeBaseFactory
                    .CreateAbcdEqualityAndSubstitutionKnowledgeBase(infp, false);

            IList<ITerm> terms = new List<ITerm> { new Constant("D") };
            var query = new Predicate("P", terms);

            IInferenceResult answer = akb.Ask(query);

            Assert.IsTrue(null != answer);
            if (expectedToFail)
            {
                Assert.IsTrue(answer.IsPossiblyFalse());
                Assert.IsFalse(answer.IsTrue());
                Assert.IsFalse(answer.IsUnknownDueToTimeout());
                Assert.IsFalse(answer.IsPartialResultDueToTimeout());
                Assert.IsTrue(0 == answer.GetProofs().Count);
            }
            else
            {
                Assert.IsFalse(answer.IsPossiblyFalse());
                Assert.IsTrue(answer.IsTrue());
                Assert.IsFalse(answer.IsUnknownDueToTimeout());
                Assert.IsFalse(answer.IsPartialResultDueToTimeout());
                Assert.IsTrue(1 == answer.GetProofs().Count);
                Assert.IsTrue(0 == answer.GetProofs()[0]
                        .GetAnswerBindings().Count);
            }
        }

        protected void TestEqualityAndSubstitutionNoAxiomsKBabcdPffaSucceeds(
                IInferenceProcedure infp, bool expectedToFail)
        {
            FOLKnowledgeBase akb = FOLKnowledgeBaseFactory
                    .CreateAbcdEqualityAndSubstitutionKnowledgeBase(infp, false);

            IList<ITerm> terms = new List<ITerm> { new Constant("A") };
            var fa = new Function("F", terms);
            terms = new List<ITerm> { fa };
            var ffa = new Function("F", terms);
            terms = new List<ITerm> { ffa };
            var query = new Predicate("P", terms);

            IInferenceResult answer = akb.Ask(query);

            Assert.IsTrue(null != answer);
            if (expectedToFail)
            {
                Assert.IsTrue(answer.IsPossiblyFalse());
                Assert.IsFalse(answer.IsTrue());
                Assert.IsFalse(answer.IsUnknownDueToTimeout());
                Assert.IsFalse(answer.IsPartialResultDueToTimeout());
                Assert.IsTrue(0 == answer.GetProofs().Count);
            }
            else
            {
                Assert.IsFalse(answer.IsPossiblyFalse());
                Assert.IsTrue(answer.IsTrue());
                Assert.IsFalse(answer.IsUnknownDueToTimeout());
                Assert.IsFalse(answer.IsPartialResultDueToTimeout());
                Assert.IsTrue(1 == answer.GetProofs().Count);
                Assert.IsTrue(0 == answer.GetProofs()[0]
                        .GetAnswerBindings().Count);
            }
        }
    }
}
